Inference at * 1 1 1 3 2 
Iof proof for Lemma nat ind tp:

.....wf..... NILNIL

1. P : {k}
2. P(0)
3. i:. P(i - 1)  P(i)
4. i : 
5. 0 < i
6. ((i - 1)  0 )  P(i - 1)
  (i  0 )   

latex

 by ((MemEqCD) 
CollapseTHEN (MemEqCD)) 

latex

C.

Definitions	t  T, x:A. B(x)
Lemmas	ge wf